Termination w.r.t. Q proof of TRS/Rubiolescanne.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))

Q is empty.

↳ QTRS

  ↳ DirectTerminationProof

Q restricted rewrite system:
The TRS R consists of the following rules:

div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))

Q is empty.

We use [23] with the following order to prove termination.

Lexicographic path order with status [19].
Quasi-Precedence:

[div₂, i_1]

Status:

i₁: [1]
div₂: [1,2]